
The following auxiliary result concerns substitutions for channels, expressions, and process variables.
Observe how the case of process variables has been relaxed so as to allow substitution 
with a process with ``smaller'' interface (in the sense of \intpr). This extra flexibility is in line
with the typing rule for located processes (rule~\rulename{t:Loc}), and will be useful later on in proofs.
%In order to prove the subject reduction theorem we need some auxiliary results. The first lemma handles substitutions.

\begin{lemma}[Substitution Lemma]\label{lem:substitution}
\quad 
\begin{enumerate}
 \item \label{subchavar}If $\judgebis{\env{\Gamma}{ \Theta}}{P}{\type{\ActS,x:\ST}{\INT}}$ then $\judgebis{\env{\Gamma}{ \Theta}}{P\sub{\cha^p}{x}}{\type{\ActS, \cha^p:\ST }{\INT}}$ %\jp{This statement should be different, I think.} \todo{check if this new formulation" is what you were thinking} 
  \item \label{subvalvar}If $\judgebis{\env{\Gamma, {x}:{\tau}}{ \Theta}}{P}{\type{\ActS}{\INT}}$ and $\typing{\Gamma}{e}{\tau}$ then $\judgebis{\env{\Gamma}{ \Theta}}{P\sub{{e}}{{x}}}{\type{\ActS}{\INT}}$. 
 % \item If $\judgebis{\env{\Gamma}{ \Theta}}{P}{\type{\ActS}{\INT}}$  then $\judgebis{\env{\Gamma}{ \Theta}}{P\sub{\cha^p}{x}}{\type{\ActS\sub{\cha^p}{x}}{\INT}}$. 
\end{enumerate}
\end{lemma}
\begin{proof}
Easily shown by induction on the structure of $P$.
\end{proof}


 As reduction may occur inside contexts, in proofs it is useful to have \emph{typed contexts}.
%building upon Def.~\ref{d:context}. 
These are 
%We thus have 
contexts in which the hole has associated typing information---concretely, the typing for processes which may fill in the hole. Defining context requires a simple extension of judgments, in the following way:
$$
\judgebis{\mathcal{H}; \env{\Gamma}{ \Theta}}{C}{\type{\ActS}{\INT}}
$$
Intuitively, $\mathcal{H}$ contains the description of the type associated to the hole in $C$.
Typing rules 
%in Tables~\ref{tab:ts} and~\ref{tab:session}
are extended in the expected way.
Because contexts have a single hole, $\mathcal{H}$ is either empty of has exactly one element.
When $\mathcal{H}$ is empty,
we write $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{ \INT }}$ instead of
$\judgebis{\cdot \, ; \env{\Gamma}{\Theta}}{P}{\type{\ActS}{ \INT }}$.
Two additional typing rules are required:
$$
\begin{array}{c}
\inferrule*[left=\rulename{t:Hole}] { }{\judgebis{\bullet_{\Gamma; \Theta \vdash \type{\ActS}{\INT}\,} ; \env{\Gamma}{\Theta}}{\bullet~}{\type{\ActS}{ \INT}}}		      
\\
\\
\inferrule*[left=\rulename{t:Fill}]		  
    {\judgebis{\bullet_{\Gamma; \Theta \vdash \type{\ActS}{\INT}\,} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS_1}{ \INT_1 }} \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{ \INT }}} {\judgebis{\env{\Gamma}{\Theta}}{C\{P\}}{\type{\ActS_1}{ \INT_1}}}
\end{array}
$$
\noindent Axiom \rulename{t:Hole} allows us to introduce typed holes into contexts. 
In rule~\rulename{t:Fill}, $P$ is a process (it does not have any holes), and $C$ is a context with a hole of type $\Gamma; \Theta \vdash \type{\ActS}{ \INT}$. 
The substitution of occurrences of $\bullet$ in $C$ with $P$, noted $C\{P\}$ 
is sound as long as the typings of $P$ coincide with those declared in $\mathcal{H}$ for $C$.
%Based on these  rules and Definitions~\ref{d:context} and~\ref{d:opcontx}, the following two auxiliary lemmas on properties of typed contexts follow easily. 
We introduce some convenient notation for typed holes.

\begin{newnotation}
Let us use $\jug, \jug', \ldots$ to range over judgments
attached to typed holes. This way,
$\bullet_\jug$ denotes the valid typed hole associated to  $\jug = \Gamma; \Theta \vdash \type{\ActS}{\INT}$.
\end{newnotation}



\begin{lemma}\label{lem:context}
 Let  $P$ and $C$ be a process and a typed context such that 
 $$\judgebis{\env{\Gamma}{\Theta}}{C\{P\}}{\type{\ActS}{ \INT}}$$ is a derivable judgment.
 There exist $\ActS_1, \INT_1$ such that 
 (i) $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT}_1}$ is a well-typed process, and
 (ii) $\ActS_1 \subseteq \ActS$ and $\INT_1 \intpr \INT$.
\end{lemma}




\begin{lemma}\label{l:ctxop}
Let $C$ be a context. %Then we have:
 Suppose $\judgebis{\bullet_{\jug} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS_C \cup \ActS_{\jug}}{ \INT_C \addelta \INT_{\jug} }}$ with $\jug = {\Gamma; \Theta \vdash \type{\ActS_{\jug}}{\INT_{\jug}}}$
is well-typed. 
Let $\jug' = {\Gamma; \Theta \vdash \type{\ActS_{\jug'}}{\INT_{\jug'}}}$.
Then 
$$\judgebis{\bullet_{\jug'} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS_C \cup \ActS_{\jug'}}{ \INT_C \addelta \INT_{\jug'} }}$$
is a derivable judgment.
\end{lemma}



\begin{theorem}[Subject Congruence] 
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ and $P \equiv Q$ then $\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\ActS}{\INT}}$.
\end{theorem}
\begin{proof}
The proof proceeds by induction on the derivation of $P \equiv Q$, with a case analysis on the last applied rule.
\qed
\end{proof}

\spnewtheorem*{notheorem}{Theorem}{\bfseries}{\itshape}


\begin{notheorem}[\ref{th:subred} Subject Reduction]\label{app:th:sr}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced and $P \pired Q$ then 
 $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS'}{\INT'}}$, for some $\INT'$ and balanced $\ActS'$.%\csub\ActS$.
\end{notheorem}


\begin{proof}
%The proof proceeds by 
By induction on the last rule applied in the reduction. %See~\ref{app:subred} for details. 
We assume that $e \downarrow c$ is a type preserving operation, for every $e$.
%\begin{description}
We examine only a few interesting cases, namely those for session establishment, runtime update, and intra-session communication; remaining cases are similar or simpler.
\paragraph{\bf Case \rulename{r:Open}} From Table~\ref{tab:redsem-full} we have:
\begin{multline*} 
C\{\nopena{u}{x:\alpha}.P_1\} \para  D\{\nopenr{u}{y:\beta}.P_2\} \pired  \\
\restr{\cha}{\big(C\{P_1\sub{\cha^+}{x} \para \que{\cha^+}{\alpha}\}  \para  D\{P_{2}\sub{\cha^-}{y} \para \que{\cha^-}{\beta}\} \big) } 
\end{multline*}
with $\alpha \cdual \beta$.
By assumption  $\judgebis{\env{\Gamma}{\Theta}}{C\{\nopena{u}{x:\alpha}.P_1\} \para  D\{\nopenr{u}{y:\beta}.P_{2}\} }{\type{\ActS}{\INT}}$
with balanced $\ActS$.
Then, by %the following derivation tree using Lemma \ref{lem:context} ($\Leftarrow$) three times,  and  
inversion on typing, using rules \rulename{t:Accept}, \rulename{t:Request}, and \rulename{t:Par} we infer
there exist $\ActS', \INT'$ such that
{%\small
\begin{equation}\label{eq:wholeopen}
\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\nopena{u}{x:\alpha}.P_1\} \para  D\{\nopenr{u}{y:\beta}.P_{2}\}}{\type{\ActS}{\INT}}}
{    \eqref{eq:typeaccept} & \eqref{eq:typerequest}}
\end{equation}
}
where, letting $\ActS = \ActS'_1 \cup \ActS'_2$, 
subtree \eqref{eq:typeaccept} is as follows: %\todo[JP:]{We should explain why $\ActS$ is different from $\ActS'$}:
\begin{equation}\label{eq:typeaccept}
\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\nopena{u}{x:\alpha}.P_1\}}{\type{\ActS_1'}{ \INT_1'\addelta u:\ST_\qual }}}		  
    { 
 	\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1}{ \INT'_1\addelta u:\ST_\qual}} & \infer{\judgebis{\env{\Gamma}{\Theta}}{\nopena{u}{x:\alpha}.P_1}{\type{\ActS_1}{ \INT_1\addelta u:\ST_\qual  }}}
  {\begin{array}{l}
     \alpha \csub \alpha'  \qquad \alpha' \cdual \beta'   \\
    \typing{\Gamma}{u}{\langle \ST'_\qual , {\STT'}_\qual \rangle} \\
   \judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS_1, x:\ST}{\INT_1}}
   \end{array}
 }}
\end{equation}
with 
\begin{equation}
\jug_1 = \Gamma; \Theta \vdash \type{\ActS_1}{\INT_1 \addelta u:\ST_\qual} \label{eq:srjug1}
\end{equation}
Then, subtree~\eqref{eq:typerequest} is as follows:
\begin{equation}\label{eq:typerequest}
\infer{\judgebis{\env{\Gamma}{\Theta}}{D\{\nopenr{u}{y:\beta}.P_{2} \}}{ \type{\ActS'_2}{ \INT'_2\addelta u:{\STT}_\qual }}}
	{\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS'_2}{ \INT'_2\addelta u:{\STT}_\qual}} &  \infer{\judgebis{\env{\Gamma}{\Theta}}{\nopenr{u}{y:\beta}.P_{2}}{ \type{\ActS_2}{ \INT_2\addelta u:{\STT}_\qual }}}
	{\begin{array}{l}
	\beta \csub \beta'  \qquad \alpha' \cdual \beta'   \\
	\typing{\Gamma}{u}{\langle \ST_\qual , {\STT}_\qual \rangle \\
	\judgebis{\env{\Gamma}{\Theta}}{P_{2}}{\type{\ActS_2, y:{\STT}}{\INT_2}}}	  
	 \end{array}
}}
 \end{equation}
 with 
 \begin{equation}
 \jug_2 = \Gamma; \Theta \vdash \type{\ActS_2}{\INT_2 \addelta u:{\STT}_\qual} \label{eq:srjug2}
 \end{equation}
By Lemma~\ref{lem:context} 
% ($\Leftarrow$) 
%there exist $\ActS_1, \ActS_2$ such that 
we have that 
$\ActS_1 \subseteq \ActS_1'$ and $\ActS_2 \subseteq \ActS_2'$. We also infer $\INT_1 \intpr \INT_1'$, $\INT_2 \intpr \INT_2'$, and $\INT' \intpr \INT$. 
 Now, using Lemma~\ref{lem:substitution}(\ref{subchavar}) on judgments for $P_1$ and $P_2$, we obtain:
 \begin{enumerate}[(a)]
 \item $\judgebis{\env{\Gamma}{ \Theta}}{P_1\sub{\cha^+}{x}}{ \type{\ActS_1, \cha^+:\ST}{\INT_1}}$.
 \item $\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :{\STT } }{\INT_2}}$.
 \end{enumerate}
%By using Lemma \ref{lem:context}($\Rightarrow$)  and typing rules \rulename{t:Par} and \rulename{t:CRes} 
%We give details for the case of $C^+$; cases for $D^+$ and $E^{++}$ follow analogously. 
We may now reconstruct the derivation given in \eqref{eq:typeaccept} using Lemma \ref{l:ctxop} and rule \rulename{t:Par}:
%$$R \triangleq {{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\} }},$$
\begin{equation}\label{eq:typeacceptsub}
\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{P_{1}\sub{\cha^+}{x} \para \que{\cha^+}{\alpha}\}}{\type{\ActS_1', \cha^+:\ST, \cha^+:\que{}{\ST}}{ \INT_1' }}}		  
    { %\begin{array}{l}
\eqref{eq:contextopen}
 &
\infer{    	\judgebis{\env{\Gamma}{ \Theta}}{P_{1}\sub{\cha^+}{x} \para \que{\cha^+}{\alpha}}{ \type{\ActS_1, \cha^+:\ST, \cha^+:\que{}{\ST}}{\INT_1}}}
{\judgebis{\env{\Gamma}{ \Theta}}{P_1\sub{\cha^+}{x}}{ \type{\ActS_1, \cha^+:\ST}{\INT_1}} & 
\judgebis{\env{\Gamma}{ \Theta}}{\que{\cha^+}{\ST}}{ \type{ \cha^+:\que{}{\ST}}{\emptyset}}}
      %5\end{array}
}
\end{equation}
with 
\begin{equation}\label{eq:contextopen}
\judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1, \cha^+:\ST, \cha^+:\que{}{\ST}\,}{ \INT'_1}} 
\end{equation}
and 
 \begin{equation}
 \jug_3 =  \Gamma; \Theta \vdash \type{\ActS_1, \cha^+:\ST, \cha^+:\que{}{\ST}}{\INT_1} \label{eq:srjug3}
 \end{equation}

For $D$, we proceed analogously from \eqref{eq:typerequest} and infer:
\begin{equation}\label{eq:typerequestsub}
 \infer{\judgebis{\env{\Gamma}{\Theta}}{D\{P_{2}\sub{\cha^-}{y} \para \que{\cha^-}{\beta} \}}{\type{\ActS'_2,\cha^- :{\STT },\cha^-:\que{}{\STT} }{\INT'_2}}}
	{
	\begin{array}{l}
	\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS'_2, \cha^-:{\STT},\cha^-:\que{}{\STT}}{ \INT'_2}} \\ \judgebis{\env{\Gamma}{ \Theta}}{P_{2}\sub{\cha^-}{y} \para \que{\cha^-}{\beta} }{\type{\ActS_2,\cha^- :{\STT },\cha^-:\que{}{\STT} }{\INT_2}}
	\end{array}
}
\end{equation}
with 
 \begin{equation}
 \jug_4 =  \Gamma; \Theta \vdash \type{\ActS_2, \cha^-:{\STT},\cha^-:\que{}{\STT}}{\INT_2} \label{eq:srjug4}
 \end{equation}
We may finally derive the type for the result of the reduction: using rules \rulename{t:Par} and \rulename{t:CRes} we obtain:
$$
	\infer{\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{C\{P_{1}\sub{\cha^+}{x} \para \que{\cha^+}{\alpha}\}  \para  D\{P_{2}\sub{\cha^-}{y} \para \que{\cha^-}{\beta} \}}}{\type{\ActS}{\INT_1' \addelta \INT_2'}}}
{\infer{
\begin{array}{ll}
 \judgebis{\env{\Gamma}{\Theta}}{{C\{P_{1}\sub{\cha^+}{x} \para \que{\cha^+}{\alpha}\}  \para  D\{P_{2}\sub{\cha^-}{y} \para \que{\cha^-}{\beta} \} }}{&\type{\ActS, \cha^+:\ST, \cha^-:{\STT},\\
 & \cha^+:\que{}{\ST}, \cha^-:\que{}{\STT} }{\\& \INT_1' \addelta \INT_2'}}
\end{array}
}{
\eqref{eq:typeacceptsub}  & 	\eqref{eq:typerequestsub}
}
}
$$

This concludes this case. 
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 
\paragraph{\bf Case \rulename{r:Upd}} From Table~\ref{tab:redsem-full} we have:
$$\begin{array}{l}
\locc{\scomponent{\locf{loc}}{P}} \para
\locdb{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}}   
\pired \qquad \\
\hfill \locc{\scomponent{\locf{loc}}{V}} \para \locd{\mathbf{0}}
\end{array}
$$
By assumption we have 
$$\judgebis{\env{\Gamma}{\Theta}}{\locc{\scomponent{\locf{loc}}{P}} \para
\locdb{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}}   
}{ \type{\ActS}{\INT}}$$
with $\ActS$ balanced.
Then, by inversion on typing, using rules
%is obtained by the following derivation tree using Lemma \ref{lem:context} ($\Leftarrow$) and  inversion on rules 
\rulename{t:Fill}, \rulename{t:Par}, \rulename{t:Adapt}, and \rulename{t:Loc} we infer:
\begin{equation}\label{eq:srupd00}
 \infer{
 \judgebis{\env{\Gamma}{\Theta}}{\locc{\scomponent{\locf{loc}}{P}} \para
\locdb{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}}   
}{ \type{\ActS}{\INT}}}{
\eqref{eq:srupd0}
&
\eqref{eq:srupd1}
}
\end{equation}
Let $\ActS = \ActS'_1 \cup \ActS'_2$ and $\INT = \INT'_1 \addelta \INT'_2$, 
subtree \eqref{eq:srupd0} is as follows:
\begin{equation}\label{eq:srupd0}
\infer{\judgebis{\env{\Gamma}{\Theta}}{\locc{\scomponent{\locf{loc}}{P}} }{ \type{\ActS'_1}{\INT'_1}}}
{\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1}{ \INT'_1 }}  & \infer{\judgebis{\env{\Gamma}{\Theta}}{\scomponent{\locf{loc}}{P}}{ \type{\ActS_1}{\INT_1}}}
{ \INT_1 \intpr \INT^*_1 & \typing{\Theta}{\locf{loc}}{\INT^*_1}
  & \judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS_1}{\INT_1} }   }}
\end{equation}
with
$\jug_1 =  \Gamma; \Theta \vdash \type{\ActS_1}{\INT_1}$,
and $\INT_1 \intpr \INT'_1$ (by Lemma~\ref{lem:context}).
Subtree \eqref{eq:srupd1} is as follows:
\begin{equation}\label{eq:srupd1}
\infer{\judgebis{\env{\Gamma}{\Theta}}{\locdb{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}}}{ \type{\ActS'_2}{\INT'_2}}}{
\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS'_2}{ \INT'_2 }} & 
\infer{\judgebis{\env{\Gamma}{\Theta}}{ \nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}}{ \type{\emptyset}{\emptyset}}}
{
\begin{array}{l}
\typing{\Theta}{\locf{loc}}{\INT}\\
\forall j \in J, \ \INT_j \intpr \INT\\
\judgebis{\env{\Gamma}{\Theta}}{Q_i}{\type{\typeque{x_{1}{:}\STT_{1}^{j}}; \cdots ;\typeque{x_{m}{:}\STT_{m}^{j}}}{\INT_j} } 
\end{array}
}}
\end{equation}
with
$\jug_2 =  \Gamma; \Theta \vdash \type{\emptyset}{\emptyset}$.
We now consider the two cases for $V$ and reconstruct the derivation after the reduction, using rules
\rulename{t:Par}, \rulename{t:Fill} and Lemma~\ref{l:ctxop}. 
The case for $V = P$ is trivial as everything is left unchanged and thus 
$$\judgebis{\env{\Gamma}{\Theta}}{\locc{\scomponent{\locf{loc}}{V}} \para
\locdb{\nil}   
}{ \type{\ActS}{\INT}}$$
Next suppose $V=Q_l\subst{\cha_1^p, \ldots, \cha^p_m\,}{\,x_1, \ldots, x_m}$. By derivation \eqref{eq:srupd1} we know that 
$$\judgebis{\env{\Gamma}{\Theta}}{Q_l}{\type{\typeque{x_{1}{:}\STT_{1}^{l}}; \cdots ;\typeque{x_{m}{:}\STT_{m}^{l}}}{\INT_l} }$$
thus applying Lemma \ref{lem:substitution}(\ref{subchavar}) we have:

\begin{equation}\label{eq:finupd}
\infer
{\judgebis{\env{\Gamma}{\Theta}}{C\{V\}  \para  D\{\nil\}}{ \type{\ActS''_1 \cup \ActS'_2}{\INT''_3 \addelta \INT_2'}}}
{\eqref{eq:finalupdate}&
\infer{\judgebis{\env{\Gamma}{\Theta}}{D\{\nil\}}{ \type{\ActS'_2}{\INT'_2}}}{
\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS_2'}{ \INT_2' }}
&\judgebis{\env{\Gamma}{\Theta}}{\nil}{ \type{\emptyset}{\emptyset}}}
}
\end{equation}

\begin{equation}\label{eq:finalupdate}
 \infer{\judgebis{\env{\Gamma}{\Theta}}{ C\{V\} }{\type{\ActS''_1}{\INT_l'}}}{
\judgebis{\bullet_{\jug_5} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS_1''}{ \INT_l' }} &
\judgebis{\env{\Gamma}{\Theta}}{ V}{\type{\typeque{x_{1}{:}\STT_{1}^{l}}; \cdots ;\typeque{x_{m}{:}\STT_{m}^{l}}}{\INT_l}}}
\end{equation}
with $\jug_5 =  \Gamma; \Theta \vdash \type{\typeque{x_{1}{:}\STT_{1}^{l}}; \cdots ;\typeque{x_{m}{:}\STT_{m}^{l}}}{\INT_l}$.
By Lemma \ref{lem:context} %($\Rightarrow$) 
we know $\INT_l \intpr \INT'_l$. Moreover by Lemma \ref{l:ctxop}, and following by application of rule \rulename{r:Upd} we have $\ActS''_1 \csub \ActS''_1$. 
This concludes the analysis for this case.



\paragraph{\bf Case \rulename{r:I/O}} From Table~\ref{tab:redsem-full} we have:
$$
\begin{array}{l}
 \locc{\outCn{\overline{\cha}^{\,p}}{v}.P_1 \para \que{\cha^p}{!(\capab).\ST} } \para \locd{\inC{\cha^{\,\overline{p}}}{{x}}.P_2 \para  \que{\cha^{\overline{p}}}{?(\capab).\STT}} 
\pired \\
\hfill
\locc{P_1 \para \que{\cha^p}{\ST}} \para  \locd{P_2\sub{{v}\,}{{x}} \para \que{\cha^{\overline{p}}}{\STT} } \quad (\ST \cdual \STT)
\end{array}
$$
By assumption, we have $\judgebis{\env{\Gamma}{\Theta}}{\locc{\outCn{\overline{\cha}^{\,p}}{v}.P_1 \para \que{\cha^p}{!(\capab).\ST} } \para \locd{\inC{\cha^{\,\overline{p}}}{{x}}.P_2 \para  \que{\cha^{\overline{p}}}{?(\capab).\STT}}  }{ \type{\ActS}{\INT}}$, with $\ActS$ balanced.
By inversion on typing, using rules 
%we obtain the following derivation that employs Lemma~\ref{lem:context} ($\Leftarrow$) three times and inversion on rules  
\rulename{t:Fill}, \rulename{t:Par}, \rulename{t:In}, and \rulename{t:Out}, we infer:
%$$
%R \triangleq C\{\outC{\cha^{\,p}}{\til{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\til{x}}.P_2\}
%$$
$$
 \infer
{
\judgebis{\env{\Gamma}{\Theta}}{C\{\outC{\cha^{\,p}}{{v}}.P_1 \para  \que{\cha^p}{!(\capab).\ST} \} \para  D\{\inC{\cha^{\,\overline{p}}}{{x}}.P_2   \para  \que{\cha^{\overline{p}}}{?(\capab).\STT} \}} {\type{\ActS'}{ \INT_1' \addelta \INT_2'}}}
{ \eqref{eq:out}
&
\eqref{eq:in}
}
$$
where:
\begin{eqnarray}
\ActS& = & \ActS_1' \cup \ActS_2', \cha^p:!({\capab}).{\ST}, \cha^p:\que{}{!({\capab}).{\ST}}, \cha^{\overline{p}}:?({\capab}).{\STT}, \cha^{\overline{p}}:\que{}{?({\capab}).{\STT}} \\
\INT & = & \INT_1' \addelta \INT_2' 
\end{eqnarray}
We have that subtree \eqref{eq:out} is as follows:
\begin{equation}\label{eq:out} 
\infer
{\judgebis{\env{\Gamma}{\Theta}}{C\{\outC{\cha^{p}}{{v}}.P_1  \para  \que{\cha^p}{!(\capab).\ST} \} } {\type{\ActS_1',  \cha^p:!({\capab}).{\ST},\cha^p:\que{}{!(\capab).\ST} }{ \INT_1' }}}
{
\eqref{eq:contextout}
 &   
\infer
{\judgebis{\env{\Gamma}{\Theta}}{\outC{\cha^p}{{v}}.P_1 \para \que{\cha^p}{!(\capab).\ST} }{\type{\ActS_1, \cha^p:!({\capab}).{\ST},\cha^p:\que{}{!(\capab).\ST}}{ \INT_1}}}
{
\judgebis{\env{\Gamma}{ \Theta}}{\que{\cha^p}{!(\capab).\ST}}{\type{  \cha^p:\que{}{!(\capab).\ST}}{\emptyset}}
&
\infer
{\judgebis{\env{\Gamma}{\Theta}}{\outC{\cha^p}{{v}}.P_1}{\type{\ActS_1, \cha^p:!({\capab}).{\ST}}{ \INT_1}}}
{\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS_1, \cha^p:{\ST}}{ \INT_1}} & \Gamma \vdash {v}:{\capab}}
}
}
\end{equation}
with
\begin{equation}\label{eq:contextout}
 \judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1, \cha^p:!({\capab}).{\ST},\cha^p:\que{}{!(\capab).\ST}{ \INT'_1 }}}
\end{equation}
and
$$
 \jug_1 =  \Gamma; \Theta \vdash \type{\ActS_1, \cha^p:!({\capab}).{\ST},\cha^p:\que{}{!(\capab).\ST}}{ \INT_1}
$$
Similarly, for  subtree \eqref{eq:in} we obtain (we show only the last step of the derivation):
\begin{equation}\label{eq:in}
 \infer{\judgebis{\env{\Gamma}{\Theta}}{ D\{\inC{\cha^{\overline{p}}}{{x}}.P_2  \para  \que{\cha^{\overline{p}}}{?(\capab).\STT} \}}{\type{ \ActS_2', \cha^{\overline{p}}:?({\capab}).{\STT}, \cha^{\overline{p}}:\que{}{{?(\capab).\STT}}}{ \INT_2'}}}
{\eqref{eq:contextin} & 
 \judgebis{\env{\Gamma}{\Theta}}{\inC{\cha^{\overline{p}}}{{x}}.P_2  \para  \que{\cha^{\overline{p}}}{?(\capab).\STT} }{\type{\ActS_2, \cha^{\overline{p}}:?({\capab}).{\STT}, \cha^{\overline{p}}:\que{}{{?(\capab).\STT}}}{ \INT_2}}}
\end{equation}
with
\begin{equation}\label{eq:contextin}
\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS_2', \cha^{\overline{p}}:?({\capab}).{\STT}, \cha^{\overline{p}}:\que{}{{?(\capab).\STT}}}{ \INT'_2 }} 
\end{equation}
and
$$
 \jug_2 =  \Gamma; \Theta \vdash \type{\ActS_2, \cha^{\overline{p}}:?({\capab}).{\STT}, \cha^{\overline{p}}:\que{}{{?(\capab).\STT}}}{ \INT_2}
$$
where Lemma~\ref{lem:context}  ensures $\ActS_1 \subseteq \ActS_1'$, $\ActS_2 \subseteq \ActS_2'$.

Now, by Lemma \ref{lem:substitution}(2)  we know $\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{{v}}{{x}}}{\type{\ActS_2, \cha^{\overline{p}}:{\STT}}{\INT_2}}$. Moreover by Lemma \ref{l:ctxop}(3) and  rules \rulename{t:Par} and \rulename{t:Fill} we obtain the following type derivations:
\begin{equation}\label{eq:output}
\infer{\judgebis{\env{\Gamma}{ \Theta}}{C\{P_1 \para \que{\cha^p}{\ST}\}}{\type{\ActS_1', \cha^p:\ST, \cha^p:\que{}{\ST}}{\INT_1'}}}
{\judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS_1', \cha^p:\ST, \cha^p:\que{}{\ST}}{\INT_1'}} 
&
\judgebis{\env{\Gamma}{ \Theta}}{P_1 \para \que{\cha^p}{\ST}}{\type{\ActS_1, \cha^p:\ST, \cha^p:\que{}{\ST}}{\INT_1}}}
\end{equation}
\begin{equation}\label{eq:input}
 \infer{\judgebis{\env{\Gamma}{\Theta}}{D\{P_2\sub{{v}\,}{{x}}  \para  \que{\cha^{\overline{p}}}{\STT}\}}{\type{\ActS_2', \cha^{\overline{p}}:{\STT}, \cha^{\overline{p}}:\que{}{{\STT}}}{ \INT_2'}}}{
\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS_2', \cha^{\overline{p}}:{\STT}, \cha^{\overline{p}}:\que{}{{\STT}}}{ \INT_2'}} 
& \judgebis{\env{\Gamma}{\Theta}}{P_2\sub{{v}\,}{{x}}  \para  \que{\cha^{\overline{p}}}{\STT} }{\type{\ActS_2, \cha^{\overline{p}}:{\STT}, \cha^{\overline{p}}:\que{}{{\STT}}}{ \INT_2}} }
\end{equation}

 $$
 \infer
{\judgebis{\env{\Gamma}{\Theta}}{C\{P_1\} \para  D\{P_2\sub{{v}\,}{{x}}\}}{\type{\ActS_1' \cup \ActS_2', \cha^p:\ST, \cha^{\overline{p}}:{\STT},  \cha^{{p}}:\que{}{{\ST}},  \cha^{\overline{p}}:\que{}{{\STT}} }{ \INT_1' \addelta \INT_2'}}}
 {\eqref{eq:output}   & \eqref{eq:input}}
$$ 
with
$$
\begin{array}{c}
 \jug_3 =  \Gamma; \Theta \vdash \type{\ActS_1, \cha^p:\ST,  \cha^{{p}}:\que{}{{\ST}}}{\INT_1}\\
 \jug_4 =  \Gamma; \Theta \vdash \type{\ActS_2, \cha^{\overline{p}}:{\STT},  \cha^{\overline{p}}:\que{}{{\STT}}}{ \INT_2}\\
 \jug_5 =  \Gamma; \Theta \vdash \type{\ActS_1' \cup \ActS_2', \cha^p:\ST, \cha^{\overline{p}}:{\STT},  \cha^{{p}}:\que{}{{\ST}},  \cha^{\overline{p}}:\que{}{{\STT}} }{ \INT_1' \addelta \INT_2'}
\end{array}
$$

Since by inductive hypothesis  $\ActS_1'$ and $\ActS_2'$ are balanced, we infer that  $\ActS_1' \cup \ActS_2', \cha^p:\ST, \cha^{\overline{p}}:{\STT}$ is balanced as well; this concludes the proof for this case.
%The other cases are similar and therefore omitted. 
\qed
\end{proof}




\begin{notheorem}[\ref{t:safety} Typing Ensures Safety and Consistency]
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced
then $P$ is update consistent and %never reduces into an error.
safe.
\end{notheorem}

\begin{proof}
%By contradiction.
Safety is a direct consequence of Theorem \ref{th:subred}.
For consistency, we assume, towards a contradiction, that there exist $P_1$, $P_2$, and $\kappa_1$ such that
\begin{enumerate}
 \item $P\pired^*P_1$, 
 \item $P_1$ has a $\kappa_1$-redex,  
 \item $P_1 \pired_{\text{upd}} P_2$, and 
 \item $P_2$ does not have a $\kappa_1$-redex.  
\end{enumerate}

Without loss of generality, 
we suppose that the reduction $P_1 \pired_{\text{upd}} P_2$ is due to a synchronization on location $l_1 \in \T$.
Since the $\kappa_1$-redex is destroyed by the update action from $P_1$ to $P_2$, the $\kappa_1$-redex in $P_1$ must necessarily be 
 a located $\kappa_1$-redex, i.e.,  in $P_1$, one or both $\kappa_1$-processes are contained inside $l_1$.
 Now, our reduction semantics (rule \rulename{r:Upd}) decrees that for such an update action to be enabled,
 the type of the process located in $l_1$ must be preserved. We also know, by Theorem~\ref{th:subred} (Subject Reduction), that $P_1$ is well-typed under a balanced
 typing $\ActS_1$.  
Hence, update steps which destroy a  
$\kappa$-redex (located and unlocated) can never be enabled from a well-typed process 
  with a balanced typing (such as $P$) nor from any of its derivatives (such as $P_1$). We thus conclude that
  well-typedness implies update consistency.
\qed
  \end{proof}

